$\forall$$T$:Type. $T$ $\subseteq\rho$ $\mathbb{Z}$ $\Rightarrow$ ($\forall$${\it bs}$, ${\it as}$:$T$ List, $x$:$T$. ($x$ $\in$ merge(${\it as}$;${\it bs}$)) $\Leftrightarrow$ ($x$ $\in$ ${\it as}$) $\vee$ ($x$ $\in$ ${\it bs}$))